Nuprl Lemma : locl_one_one
11,40
postcript
pdf
a
,
b
:Id. (locl(
a
) = locl(
b
)
Knd)
(
a
=
b
)
latex
Definitions
Id
,
t
T
,
IdLnk
,
,
P
Q
,
x
:
A
.
B
(
x
)
,
locl(
a
)
,
Knd
Lemmas
IdLnk
wf
,
Id
wf
origin
a, b:Id. (locl(a) = locl(b) 
Knd) 
(a = b) a, b:Id. (locl(a) = locl(b) Knd) (a = b) T
Qx:A. B(x)